Search for: All records

Chess endgame tables encode unapproximated game- theoretic values of endgame positions. The speed at which information is retrieved from these tables and their representation size are major limiting factors in their effective use. We explore and make novel extensions to three alternatives (decision trees, decision diagrams, and logic minimization) to the currently preferred implementation (Syzygy) for representing such tables. Syzygy is most compact, but also slowest at handling queries. Two-level logic minimization works well when the full compression algorithm can be run. Decision DAGs and multiterminal binary decision diagrams are comparable and offer the best querying times, with decision diagrams providing better compression. 

We introduce RexBDDs, binary decision diagrams (BDDs) that exploit reduction opportunities well beyond those of reduced ordered BDDs, zero-suppressed BDDs, and recent proposals integrating multiple reduction rules. RexBDDs also leverage (output) complement flags and (input) swap flags to potentially decrease the number of nodes by a factor of four. We define a reduced form of RexBDDs that ensures canonicity, and use a set of benchmarks to demonstrate their superior storage and runtime requirements compared to previous alternatives. 

Binary decision diagrams (BDDs) have been a huge success story in hardware and software verification and are increasingly applied to a wide range of combinatorial problems. While BDDs can encode boolean-valued functions of boolean-valued variables, many BDD variants have been proposed, not just to improve their efficiency, but to manage multivalued domains (a straightforward extension), multivalued ranges (using several competitive alternatives), and two-dimensional data (relations and matrices instead of sets or vectors). Orthogonally to these extensions, much effort has been spent on variable order heuristics, an essential aspect that can affect memory and time requirements by up to an exponential factor. We survey some of these exciting results and discuss some fruitful research directions for further work. Index Terms—Binary decision diagrams, canonicity, discrete function encoding, variable order heuristics, Markov chains 

Generating the state space of any finite discrete-state system using symbolic algorithms like saturation requires the use of decision diagrams or compatible structures for encoding its reachability set and transition relations. For systems that can be formally expressed using ordinary Petri Nets(PN), implicit relations, a static alternative to decision diagram-based representation of transition relations, can significantly improve the performance of saturation. However, in practice, some systems require more general models, such as self-modifying Petri nets, which cannot currently utilize implicit relations and thus use decision diagrams that are repeatedly rebuilt to accommodate the changing bounds of the system variables, potentially leading to overhead in saturation algorithm. This work introduces a hybrid representation for transition relations, that combines decision diagrams and implicit relations, to reduce the rebuilding overheads of the saturation algorithm for a general class of models. Experiments on several benchmark models across different tools demonstrate the efficiency of this representation. 

The size of a BDD heavily depends on its variable order. Significant efforts have been made to find good variable orders, statically or dynamically. This paper concentrates on a related issue, transforming a BDD from one variable order to another, as needed when an application must cope with BDDs having different variable orders. Instead of rebuilding BDDs as done in previous work, we accomplish such transformation through a sequence of adjacent variable swaps. Since there are many ways to schedule these swaps, we propose and compare several heuristics to determine good schedules.